Nuprl Lemma : w-es_wf
11,40
postcript
pdf
w
:World,
p
:FairFifo. ES(
w
)
ES
latex
Definitions
t
T
,
,
P
Q
,
x
:
A
.
B
(
x
)
,
S
T
Lemmas
int
inc
rationals
,
nat
wf
,
rationals
wf
,
subtype
rel
transitivity
origin
w:World, p:FairFifo. ES(w) 
ES w:World, p:FairFifo. ES(w) ES T
Qx:A. B(x)
T